X, Y:(), k:, y:( List).
(k  ||y||)
 (q-linear(k;j.X(j) + Y(j);y) = (q-linear(k;j.X(j);y) + q-linear(k;j.Y(j);y))  ) 

latex

Definitions	i  j , , False, A, P & Q, True, T, x. t(x), P  Q, P  Q, t  T, x(s), A  B, P  Q, , x:A. B(x),
Lemmas	qadd ac 1 q, mon assoc q, qmul comm qrng, qmul over plus qrng, ge wf, nat properties, q-linear wf, select wf, qmul wf, q-linear-unroll, length wf1, le wf, true wf, squash wf, qadd wf, q-linear-base, rationals wf, nat wf